$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)), ${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $X$:Interface(${\it ds}$;${\it da}$;$A$).
\\[0ex]interface{-}compose($f$;$X$) $\in$ Interface(${\it ds}$;${\it da}$;$B$)